T:Type, L:T List, f:(||L||||L||), i:||L||. (L o f)[i] = L[f(i)]  T 

latex

Definitions	x:A. B(x), ij, ||as||, {i..j}, t  T, P  Q, l[i], False, A, P & Q, AB, i  j < k, , P  Q, P  Q, (L o f)
Lemmas	int seg wf, mklist select, length wf1, select wf, non neg length